DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2021.18

Formalized Haar Measure

Authors: Floris van Doorn

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

We describe the formalization of the existence and uniqueness of the Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean’s mathematical library mathlib, and discuss the construction of product measures and the proof of Fubini’s theorem for the Bochner integral.

Cite as

Floris van Doorn. Formalized Haar Measure. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{vandoorn:LIPIcs.ITP.2021.18,
  author =	{van Doorn, Floris},
  title =	{{Formalized Haar Measure}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.18},
  URN =		{urn:nbn:de:0030-drops-139139},
  doi =		{10.4230/LIPIcs.ITP.2021.18},
  annote =	{Keywords: Haar measure, measure theory, Bochner integral, Lean, interactive theorem proving, formalized mathematics}
}

Document

DOI: 10.4230/LIPIcs.ITP.2019.19

A Formalization of Forcing and the Unprovability of the Continuum Hypothesis

Authors: Jesse Michael Han and Floris van Doorn

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract

We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model.

Cite as

Jesse Michael Han and Floris van Doorn. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{han_et_al:LIPIcs.ITP.2019.19,
  author =	{Han, Jesse Michael and van Doorn, Floris},
  title =	{{A Formalization of Forcing and the Unprovability of the Continuum Hypothesis}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.19},
  URN =		{urn:nbn:de:0030-drops-110742},
  doi =		{10.4230/LIPIcs.ITP.2019.19},
  annote =	{Keywords: Interactive theorem proving, formal verification, set theory, forcing, independence proofs, continuum hypothesis, Boolean-valued models, Lean}
}

Search Results

Documents authored by van Doorn, Floris

Formalized Haar Measure

Abstract

Cite as

A Formalization of Forcing and the Unprovability of the Continuum Hypothesis

Abstract

Cite as

Thanks for your feedback!

Could not send message